(*************************************************************************)
(** Simply-typed Scalina  in Coq.    Infrastructure                      *)
(** Author: Adriaan Moors, 2008                                          *)
(*************************************************************************)

(** Based on the Coq tutorial at POPL 2008, see
    "Engineering Formal Metatheory", Aydemir, Charguéraud, Pierce,
    Pollack, Weirich. POPL 2008.

    Tutorial authors: Brian Aydemir and Stephanie Weirich, with help
    from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey
    Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic.  Adapted from
    code by Arthur Charguéraud.
*)

Set Implicit Arguments.
Require Import Metatheory Scalina_Definitions Scalina_Induction support.
Require Import List.

(** There are two important advantages of the locally nameless
    representation:
     - Alpha-equivalent terms have a unique representation, 
       we're always working up to alpha-equivalence.
     - Operations such as free variable substitution and free
       variable calculation have simple recursive definitions
      (and therefore are simple to reason about).

    Weighed against these advantages are two drawbacks:
     - The [exp] datatype admits terms, such as [abs 3], where
       indices are unbound. 
       A term is called "locally closed" when it contains 
       no unbound indices. 
     - We must define *both* bound variable & free variable 
       substitution and reason about how these operations 
       interact with eachother.
    
*)


(*************************************************************************)
(** * Substitution *)
(*************************************************************************)

(** Substitution replaces a free variable with a term.  The definition
    below is simple for two reasons:
      - Because bound variables are represented using indices, there
        is no need to worry about variable capture.
      - We assume that the term being substituted in is locally
        closed.  Thus, there is no need to shift indices when
        passing under a binder.
*)

Fixpoint subst_tm (z : var) (u : tm) (e : tm) {struct e} : tm :=
  match e with
    | bvar i => bvar i
    | fvar x => if x == z then u else (fvar x)
    | sel e1 l => sel (subst_tm z u e1) l
    | new T => new (subst_tp z u T)
  end

with subst_tp (z : var) (u : tm) (e : tp) {struct e} : tp :=
  match e with
    | tp_single p => tp_single (subst_tm z u p)
    | tp_struct self mems => tp_struct (option_map (subst_tp z u) self) (List.map (subst_mem z u) mems)
  end

with subst_mem (z : var) (u : tm) (e : mem) {struct e} : mem :=
  match e with
    | mtm l mut T rhs => mtm l mut (subst_tp z u T)  (option_map (subst_tm z u) rhs)
  end.

(** The Fixpoint keyword defines a Coq function. As all functions in 
    Coq must be total, the annotation [{struct e}] indicates the termination 
    metric---all recursive calls in this definition are made to
    arguments that are structurally smaller than [e].
*)

(* Note also that subst uses the notation [x == z] for
   decidable var equality. (This notation is defined in
   [Metatheory].)
*)


(** We define a notation for free variable substitution that mimics
    standard mathematical notation. *)

Notation "[ z ~> u ] e" := (subst_tm z u e) (at level 68).
Notation "[ z ~tp> u ] t" := (subst_tp z u t) (at level 68).
Notation "[ z ~mem> u ] m" := (subst_mem z u m) (at level 68).
Definition subst_mems z u ms := (map (subst_mem z u) ms).
Notation "[ z ~mems> u ] ms" := (subst_mems z u ms) (at level 68).
Notation "[ z ~env> u ] E" := (Env.map (subst_tp z u) E) (at level 68).




(* ********************************************************************** *)
(** ** Instantiation of tactics *)

(** Tactic [gather_vars] returns a set of variables occurring in
    the context of proofs, including domain of environments and
    free variables in terms mentionned in the context. *)

Ltac gather_vars :=
  let A := gather_vars_with (fun x : vars => x) in
  let B := gather_vars_with (fun x : var => {{ x }}) in
  let C := gather_vars_with (fun x : env => dom x) in
  let D := gather_vars_with (fun x : tm => fv_tm x) in
  let E := gather_vars_with (fun x : tp => fv_tp x) in
  let F := gather_vars_with (fun x : mem => fv_mem x) in (*TODO: lists of members,. *)
  let G := gather_vars_with (fun x : list mem => fv_mems x) in (*TODO: lists of members,. *)
  constr:(A \u B \u C \u D \u E \u F \u G).

(** Tactic [pick_fresh x] adds to the context a new variable x
    and a proof that it is fresh from all of the other variables
    gathered by tactic [gather_vars]. *)

Ltac pick_fresh Y :=
  let L := gather_vars in (pick_fresh_gen L Y).

(** Tactic [apply_fresh T as y] takes a lemma T of the form 
    [forall L ..., (forall x, x \notin L, P x) -> ... -> Q.]
    instanciate L to be the set of variables occuring in the
    context (by [gather_vars]), then introduces for the premise
    with the cofinite quantification the name x as "y" (the second
    parameter of the tactic), and the proof that x is not in L. *)

Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
  apply_fresh_base T gather_vars x.

Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
  apply_fresh T as x; auto*.

Hint Constructors lc_tp lc_mem lc_tm lc_mems value red.

Lemma lc_mems_forAll: forall ms, lc_mems ms -> list_forAll (List.map lc_mem ms).
Proof.
  intros.
  induction ms.
    simpl. auto. 
    simpl in *. inversion H. 
      split. 
        assumption.
        apply IHms. assumption.
Qed.

Lemma lc_mems_forAll_conv: forall ms, list_forAll (List.map lc_mem ms) -> lc_mems ms.
Proof.
  intros.
  induction ms.
    auto. 
    simpl in *. inversion H.   apply lc_cons.
        assumption.
        apply IHms. assumption.
Qed.




(** At this point we are still stuck because the IH concerns
   [open e x] instead of [e]. The result that
   we need is that if an index substitution has no effect for
   an opened term, then it has no effect for the raw term (as long
   as we are *not* substituting for 0, hence S k below).
<<
   open e x = {S k ~> u}(open e x)  -> e = {S k ~> u} e
>>
   In other words, expanding the definition of open:
<<
   {0 ~> x}e = {S k ~> u}({0 ~> x} e)  -> e = {S k ~> u} e
>>
   Of course, to prove this result, we must generalize
   0 and S k to be any pair of inequal numbers to get a strong
   enough induction hypothesis for the abs case.
 *)



Lemma open_rec_lc_core : 
  (forall e j v i u, i <> j ->  {j ~> v} e = {i ~> u} ({j ~> v} e) -> {i ~> u} e = e) /\ 
  (forall t j v i u, i <> j ->   {j ~tp> v} t = {i ~tp> u} ({j ~tp> v} t) -> {i ~tp> u} t = t) /\ 
  (forall m j v i u, i <> j ->   {j ~mem> v} m = {i ~mem> u} ({j ~mem> v} m) -> {i ~mem> u} m = m) /\ 
  (forall ms j v i u, i <> j ->  {j ~mems> v} ms = {i ~mems> u} ({j ~mems> v} ms) -> {i ~mems> u} ms = ms).
Proof.
  apply tm_tp_mem_mutual_ind;  simpl in *.  
(*  induction e; intros j v i u Neq H; simpl in *.*)

  (*case bvar*)
      intros n j v i u Neq H. destruct (j === n);  destruct (i === n).
      (*Case "j = n = i".*)
        subst n. intros. destruct Neq. auto.
      (*Case "j = n, i <> n".*)
        auto.
      (*Case "j <> n, i = n".*)
        subst n. simpl in H. destruct (i === i). auto. destruct n. auto.
      (*Case "j <> n, i <> n".*)
        auto.
 
   (* case fvar *)
     auto.

   (* case sel *) 
     intros. f_equal. inversion H1. eapply H; eauto.

   (* case new *) 
     intros. f_equal. inversion H1. eapply H; eauto.

   (* case tp_single *)
     intros. f_equal. inversion H1. eapply H; eauto.
   (* case tp_struct *)
     intros. f_equal. inversion H1. fold ({i+1 ~mems> u} ms). 
     fold ({j+1 ~mems> v} ms) in H3. fold ({i+1 ~mems> u} ({j + 1 ~mems> v}ms)) in H3.
     assert (i+1 <> j+1) as DiffS by omega.
     apply (H (j+1) v (i+1) u DiffS); auto*.

    intros.  f_equal. f_equal. eapply H. apply H1. inversion H2. apply H4.
      fold ({i+1 ~mems> u} ms).
      fold ({j+1 ~mems> v} ms) in H2. fold ({i+1 ~mems> u} ({j + 1 ~mems> v}ms)) in H2.
     assert (i+1 <> j+1) as DiffS by omega.
     apply (H0 (j+1) v (i+1) u DiffS); auto*.
     inversions* H2.

   (* case mtm *)
     intros. f_equal. inversion H1. eapply H. apply H0. apply H3.

     intros. f_equal. inversion H2. eapply H. apply H1. apply H4.
     f_equal. inversion H2. eapply H0. apply H1. apply H5.

    auto.

    intros. f_equal. eapply H; eauto. inversions* H2.  eapply H0; eauto. inversions* H2.
Qed.


(* because of the mutual induction, can't use generalize dependent -- distribute the forall k over the conjunction manually *)
Lemma open_rec_lc : forall u,
  (forall e, lc_tm e -> forall k, {k ~> u} e = e) /\
  (forall e, lc_tp e -> forall k, {k ~tp> u} e = e) /\
  (forall e, lc_mem e ->  forall k, {k ~mem> u} e = e) /\
  (forall e, lc_mems e ->  forall k, {k ~mems> u} e = e).

Proof.
  intros u.
  apply lc_tm_tp_mem_mems_mutual_ind; try intros; simpl; do 2 f_equal; auto; 
    [rename H into H' | rename H0 into H'];
  repeat  
    (fold ({k+1 ~mems> u} mems); pick_fresh x;  assert (x \notin L) as FrX by auto;
     pose (H' x FrX (k+1)); fold ({0 ~mems> x} mems) in e; destruct open_rec_lc_core as [_ [_ [_ HOpenCore]]];
     assert ((k+1) <> 0) as Diff by omega; apply (@HOpenCore mems 0 x (k+1) u Diff); auto*).
Qed.


Lemma subst_open_rec : forall e1 e2 x,
  lc_tm e1 -> 
  (forall u k, [x ~> e1] ({k ~> e2} u) = {k ~> [x ~> e1] e2} ([x ~> e1] u)) /\
  (forall u k, [x ~tp> e1] ({k ~tp> e2} u) = {k ~tp> [x ~> e1] e2} ([x ~tp> e1] u)) /\
  (forall u k, [x ~mem> e1] ({k ~mem> e2} u) = {k ~mem> [x ~> e1] e2} ([x ~mem> e1] u)) /\
  (forall u k, [x ~mems> e1] ({k ~mems> e2} u) = {k ~mems> [x ~> e1] e2} ([x ~mems> e1] u)).
Proof.
  intros e1 e2 x Hlc.
  apply tm_tp_mem_mutual_ind;  simpl in *; try (intros; f_equal; auto).
 
  destruct (k === n); simpl in *; trivial.

  destructs (open_rec_lc ([x ~> e1]e2)).
  destruct (a == x); try symmetry; auto*.

  unfold open_rec_mems in *. unfold subst_mems in *.
  pose (HS := H (k+1)). do 2 rewrite map_map in *. trivial.

  f_equal.
  unfold open_rec_mems in *. unfold subst_mems in *.
  pose (HS := H (k)). trivial.

  unfold open_rec_mems in *. unfold subst_mems in *.
  pose (HS := H0 (k+1)). do 2 rewrite map_map in *. trivial.

  f_equal; auto.
Qed.


Lemma subst_open_var : forall e1 (x y: var),
  y <> x ->
  lc_tm e1 -> 
  (forall u, open ([x ~> e1] u) y = [x ~> e1] (open u y)) /\
  (forall u, open_tp ([x ~tp> e1] u) y = [x ~tp> e1] (open_tp u y)) /\
  (forall u, open_mem ([x ~mem> e1] u) y = [x ~mem> e1] (open_mem u y)) /\
  (forall u, open_mems ([x ~mems> e1] u) y = [x ~mems> e1] (open_mems u y)).
Proof.
  intros e1 x y HNeq Hlc.   
  unfold open. unfold open_tp. unfold open_mem. 

  splits; destructs (@subst_open_rec e1 y x Hlc); intros; symmetry; simpl in *; 
    (destruct (y==x);[
      simpl; subst y;  destruct HNeq;  auto|
      first [auto; apply (H3 u 0)] ]).    
Qed.





Lemma subst_fresh : forall (x : var) u,
  (forall e, x \notin fv_tm e -> [x ~> u] e = e) /\ 
  (forall t, x \notin fv_tp t -> [x ~tp> u] t = t) /\ 
  (forall m, x \notin fv_mem m -> [x ~mem> u] m = m) /\ 
  (forall ms, list_forAll (List.map (fun m => x \notin fv_mem m -> [x ~mem> u] m = m) ms)).
Proof.
  intros x u.
  apply tm_tp_mem_mutual_ind; intros; simpl; f_equal; simpl in *; auto*; first [

  (* case bvar *)
    destruct (a == x); auto*; simpl in *; subst; rewrite (notin_singleton x x) in H; auto* |

  (* case tp_struct *)
    apply list_forAll_eq_dist; apply (list_forAll_MP ms _ _ H); simpl in *; apply notinUnion_forAll_notin; auto |
    apply list_forAll_eq_dist; apply (list_forAll_MP ms _ _ H0); simpl in *; apply notinUnion_forAll_notin; auto |
     
    f_equal; auto*].
Qed.


Lemma subst_fresh_mems: forall (x : var) u ms,
  x \notin fv_mems ms -> [x ~mems> u] ms = ms.
Proof.
  introv Fr.
  destructs (@subst_fresh x u).
  pose (H3 ms).
  unfold subst_mems.
  apply list_forAll_eq_dist. apply (list_forAll_MP ms _ _ l); trivial.
  induction ms; simpl in *; auto*.
  unfold fv_mems in Fr. simpl in Fr. rewrite foldUnionAssoc in Fr. 
  split. auto. apply notinUnion_forAll_notin. auto.
Qed.

Lemma subst_intro_tm : forall x m u, 
  x \notin (fv_tm m) -> lc_tm u ->
  open m u = [x ~> u](open m (fvar x)).
Proof.
  introv Fr Wu.
  destructs (@subst_open_rec u x x). assumption. unfold open. pose (Heq0 := (H m 0)). rewrite Heq0.
  destructs (subst_fresh x u). pose (Heq := (H2 m Fr)). simpl. case_var*. rewrite Heq. reflexivity.
Qed.

Lemma subst_intro_tp : forall x m u, 
  x \notin (fv_tp m) -> lc_tm u ->
  open_tp m u = [x ~tp> u](open_tp m (fvar x)).
Proof.
  introv Fr Wu.
  destructs (@subst_open_rec u x x). assumption. unfold open_tp. pose (Heq0 := (H1 m 0)). rewrite Heq0.
  destructs (subst_fresh x u). pose (Heq := (H5 m Fr)). simpl. case_var*. rewrite Heq. reflexivity.
Qed.

Lemma subst_intro_mem : forall x m u, 
  x \notin (fv_mem m) -> lc_tm u ->
  open_mem m u = [x ~mem> u](open_mem m (fvar x)).
Proof.
  introv Fr Wu.
  destructs (@subst_open_rec u x x). assumption. unfold open_mem. pose (Heq0 := (H0 m 0)). rewrite Heq0.
  destructs (subst_fresh x u). pose (Heq := (H4 m Fr)). simpl. case_var*. rewrite Heq. reflexivity.
Qed.

Lemma subst_intro_mems : forall x m u, 
  x \notin (fv_mems m) -> lc_tm u ->
  open_mems m u = [x ~mems> u](open_mems m (fvar x)).
Proof.
  introv Fr Wu.
  destructs (@subst_open_rec u x x). assumption. pose (Heq0 := (H3 m 0)). unfold open_mems.  fold ({0 ~mems> x}m). rewrite Heq0.
  simpl. case_var*. rewrite (@subst_fresh_mems x u _ Fr). fold ({0 ~mems> u} m). reflexivity.
Qed.


Lemma subst_lc : forall (x : var) u,
  lc_tm u ->
  (forall e,  lc_tm e -> lc_tm ([x ~> u] e)) /\
  (forall e,  lc_tp e -> lc_tp ([x ~tp> u] e)) /\
  (forall e,  lc_mem e -> lc_mem ([x ~mem> u] e)) /\
  (forall e,  lc_mems e -> lc_mems ([x ~mems> u] e)).
Proof. 
  intros x u Hu.
  apply lc_tm_tp_mem_mems_mutual_ind; intros; simpl; auto*; try first[
    destruct (x0 == x); auto* |

    first[apply lc_struct_noself with (L:={{x}} \u L)|
          apply lc_struct_self with (L := L \u {{x}});auto*]; intros;
      fold ([x ~mems> u] mems); fold (open_mems ([x ~mems> u]mems) x0);
      assert (x0 \notin L) as Fr0 by auto*;
      first[pose (LcMs:= H x0 Fr0)| pose (LcMs:= H0 x0 Fr0)]; fold (open_mems mems x0) in LcMs; 
      assert (x0 <> x) as Diff by auto*; destruct (@subst_open_var u x x0 Diff Hu) as [_ [_ [_ HOpen]]];
      rewrite HOpen; assumption].
Qed.

Lemma lc_open_tm: forall (x: var) t' e,
  lc_tm t' -> x \notin fv_tm e -> lc_tm (e ^ x) -> lc_tm (e ^^ t').
Proof.
  intros.
  rewrite (@subst_intro_tm x e t'); trivial.
  destructs (subst_lc x H); auto*.
Qed.

Lemma lc_open_tp: forall (x: var) t' e,
  lc_tm t' -> x \notin fv_tp e -> lc_tp (open_tp e x) -> lc_tp (open_tp e t').
Proof.
  intros.
  rewrite (@subst_intro_tp x e t'); trivial.
  destructs (subst_lc x H); auto*.
Qed.

Lemma lc_open_mems: forall (x: var) t' e,
  lc_tm t' -> x \notin fv_mems e -> lc_mems (open_mems e x) -> lc_mems (open_mems e t').
Proof.
  intros.
  rewrite (@subst_intro_mems x e t'); trivial.
  destructs (subst_lc x H); auto*.
Qed.


(*
(* case lc_mems *)
  apply lc_mems_forAll_conv.
  pose (lc_mems_forAll LcOpen).
  unfold open_mems in *. rewrite map_map in *.
  apply under_forAll_map_retain_in with (f :=  (fun m : mem => lc_mem ({0 ~mem> t}m))) (g := (fun m : mem => lc_mem ({0 ~mem> t'}m))).
  intros m Hm_in_ms Hlcmem. 

(*  destructs (lc_open_some_lc_open_any x). auto*.*)
  assert (x \notin fv_mem m) as Hnotinm. assert (x \notin fv_mems ms) as Hx_notin_ms. auto*. unfold fv_mems in Hx_notin_ms.


  pose (notinUnion_forAll_notin ms fv_mem Hx_notin_ms). 

  apply (forAll_implies_forIn ms m (fun m => x \notin fv_mem m) l0). assumption.

  pose (Heq := @subst_intro_mem x m t Hnotinm H).
  
  unfold open_mem in Heq.
  rewrite Heq.
  destructs (subst_lc x H).
  auto*.
*)




(********************************)
(* additional freshness results *)
(********************************)


Lemma fv_open_var : forall (y x : var), x <> y ->
  (forall e n, x \notin fv_tm (open_rec_tm n y e) -> x \notin fv_tm e) /\ 
  (forall t n, x \notin fv_tp (open_rec_tp n y t) -> x \notin fv_tp t) /\ 
  (forall m n, x \notin fv_mem (open_rec_mem n y m) -> x \notin fv_mem m) /\ 
  (forall ms n, x \notin fv_mems (open_rec_mems n y ms) -> x \notin fv_mems ms).
Proof.
  introv Neq.
  apply tm_tp_mem_mutual_ind; intros; simpl; auto*; try (simpl in *; pose (H n); auto*); try notin_simpl; auto*.

  assert (x \notin fold_left (fun (ats : vars) (m : mem) => ats \u fv_mem m)
         (map (open_rec_mem (n + 1) y) ms) {}) as Hms by auto.
  fold (fv_mems ms).
  fold ({n+1 ~mems> y}ms) in Hms.
  fold (fv_mems ({n+1 ~mems> y}ms)) in Hms.
  apply (H (n+1)); trivial.

  assert ( x \notin
       fv_tp ({n ~tp> y}t)) as HSelfTp by auto.
  assert (x \notin fold_left (fun (ats : vars) (m : mem) => ats \u fv_mem m)
         (map (open_rec_mem (n + 1) y) ms) {}) as Hms by auto.
  fold (fv_mems ms).
  fold ({n+1 ~mems> y}ms) in Hms.
  fold (fv_mems ({n+1 ~mems> y}ms)) in Hms.
  apply (H0 (n+1)); trivial.

  pose (H0 n). auto.

  unfold fv_mems in H1. simpl in H1.
    rewrite (foldUnionAssoc fv_mem ({n ~mems> y}Ts) ({n ~mem> y}T)) in H1.
    assert ( x \notin fv_mem ({n ~mem> y}T)) as HT by auto.
    assert ( x \notin
       fold_left (fun (xs : vars) (x : mem) => xs \u fv_mem x)
         ({n ~mems> y}Ts) {}) as HTs by auto.
    pose (HT':= H n HT).
    pose (HTs':= H0 n HTs).
    unfold fv_mems. simpl.  rewrite (foldUnionAssoc fv_mem (Ts) (T)).
    notin_simpl; trivial.
Qed.

Lemma fv_open_var_conv : forall (x : var) u, x \notin fv_tm u ->
  (forall e n, x \notin fv_tm e -> x \notin fv_tm (open_rec_tm n u e)) /\ 
  (forall t n, x \notin fv_tp t -> x \notin fv_tp (open_rec_tp n u t)) /\ 
  (forall m n, x \notin fv_mem m -> x \notin fv_mem (open_rec_mem n u m)) /\ 
  (forall ms n, x \notin fv_mems ms -> x \notin fv_mems (open_rec_mems n u ms)).
Proof.
  introv Neq.
  apply tm_tp_mem_mutual_ind; intros; simpl; auto*; try (simpl in *; pose (H n); auto*); try notin_simpl; auto*.

  destruct (n0 === n); simpl in *; auto*.

  fold ({n+1 ~mems> u}ms). fold (fv_mems ({n+1 ~mems> u}ms)). fold (fv_mems ms) in H0.
  apply (H (n+1));auto*.

  fold ({n+1 ~mems> u}ms). fold (fv_mems ({n+1 ~mems> u}ms)). fold (fv_mems ms) in H1.
  apply (H0 (n+1));auto*.
 
  unfold fv_mems in H1. simpl in H1. rewrite foldUnionAssoc in H1. fold (fv_mems Ts) in H1.
  unfold fv_mems. simpl. rewrite foldUnionAssoc.
  fold (fv_mems ({n ~mems> u}Ts)).
  assert (x \notin fv_mem ({n ~mem> u}T)) by (apply (H n); auto*).
  assert (x \notin fv_mems ({n ~mems> u}Ts)) by (apply (H0 n); auto*).
  auto*.
Qed.

Lemma fv_intro_subst: forall z u,
   z \notin fv_tm u
-> (forall t, z \notin fv_tm ([z ~> u]t)) /\
   (forall t, z \notin fv_tp ([z ~tp> u]t)) /\
   (forall t, z \notin fv_mem ([z ~mem> u]t)) /\
   (forall t, z \notin fv_mems ([z ~mems> u]t)).
Proof.
  introv ZNotInU.
  apply tm_tp_mem_mutual_ind; intros; simpl; auto*.
  
  destruct (a==z). subst. trivial.
  simpl in *. auto*.
 
  fold ([z ~mems> u]ms).
  fold ( fv_mems ([z ~mems> u]ms)).
  notin_solve; auto*.

  fold ([z ~mems> u]ms).
  fold ( fv_mems ([z ~mems> u]ms)).
  notin_solve; auto*.

  unfold fv_mems. simpl. auto*.
  unfold fv_mems. simpl. 

  rewrite (foldUnionAssoc fv_mem ([z ~mems> u]Ts) ([z ~mem> u]T)).
  fold ( fv_mems ([z ~mems> u]Ts)).
  notin_solve; auto*.
Qed.


Lemma fv_intro_subst_2: forall x z u,
   x <> z
-> x \notin fv_tm u
-> (forall t, x \notin fv_tm t -> x \notin fv_tm ([z ~> u]t)) /\
   (forall t, x \notin fv_tp t -> x  \notin fv_tp ([z ~tp> u]t)) /\
   (forall t, x \notin fv_mem t -> x  \notin fv_mem ([z ~mem> u]t)) /\
   (forall t, x \notin fv_mems t -> x  \notin fv_mems ([z ~mems> u]t)).
Proof.
  introv Neq ZNotInU.
  apply tm_tp_mem_mutual_ind; intros; simpl; auto*.

  destruct (a==z). subst. trivial.
  simpl in *. auto*.
 
  fold ([z ~mems> u]ms).
  fold ( fv_mems ([z ~mems> u]ms)).
  simpl in H0.   fold ( fv_mems (ms)) in H0. assert (x \notin fv_mems ms) by auto*. pose (H H1).
  notin_solve; auto*.

  fold ([z ~mems> u]ms).
  fold ( fv_mems ([z ~mems> u]ms)).
  simpl in H1. fold ( fv_mems (ms)) in H1. assert ( x \notin fv_tp t) by auto*.  assert ( x \notin fv_mems ms) by auto*.
  pose (H H2). pose (H0 H3).
  notin_solve; auto*.

  simpl in *. assert ( x \notin fv_tp t) by auto*. pose (H H1). notin_solve;auto*.
  simpl in *. assert ( x \notin fv_tp t) by auto*. assert ( x \notin fv_tm rhs) by auto*. 
  pose (H H2). pose (H0 H3). notin_solve;auto*.

  unfold fv_mems. simpl. 
  rewrite (foldUnionAssoc fv_mem ([z ~mems> u]Ts) ([z ~mem> u]T)).
  fold ( fv_mems ([z ~mems> u]Ts)).
  unfold fv_mems in H1. simpl in H1. rewrite (foldUnionAssoc fv_mem (Ts) (T)) in H1.
  fold ( fv_mems (Ts)) in H1.
  assert (x \notin fv_mems Ts) by auto*.
  assert (x \notin fv_mem T) by auto*.
  pose (H H3). pose (H0 H2).
  notin_solve; auto*.
Qed.


(*
*** Local Variables: ***
*** coq-prog-args: ("-emacs-U"  "-I" "../lib" "-I" "../metatheory") ***
*** End: ***
*)